Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		p(s(x))	→ x
2:		plus(x,0)	→ x
3:		plus(0,y)	→ y
4:		plus(s(x),y)	→ s(plus(x,y))
5:		plus(s(x),y)	→ s(plus(p(s(x)),y))
6:		plus(x,s(y))	→ s(plus(x,p(s(y))))
7:		times(0,y)	→ 0
8:		times(s(0),y)	→ y
9:		times(s(x),y)	→ plus(y,times(x,y))
10:		div(0,y)	→ 0
11:		div(x,y)	→ quot(x,y,y)
12:		quot(0,s(y),z)	→ 0
13:		quot(s(x),s(y),z)	→ quot(x,y,z)
14:		quot(x,0,s(z))	→ s(div(x,s(z)))
15:		div(div(x,y),z)	→ div(x,times(y,z))
16:		eq(0,0)	→ true
17:		eq(s(x),0)	→ false
18:		eq(0,s(y))	→ false
19:		eq(s(x),s(y))	→ eq(x,y)
20:		divides(y,x)	→ eq(x,times(div(x,y),y))
21:		prime(s(s(x)))	→ pr(s(s(x)),s(x))
22:		pr(x,s(0))	→ true
23:		pr(x,s(s(y)))	→ if(divides(s(s(y)),x),x,s(y))
24:		if(true,x,y)	→ false
25:		if(false,x,y)	→ pr(x,y)

There are 20 dependency pairs:


26:		PLUS(s(x),y)	→ PLUS(x,y)
27:		PLUS(s(x),y)	→ PLUS(p(s(x)),y)
28:		PLUS(s(x),y)	→ P(s(x))
29:		PLUS(x,s(y))	→ PLUS(x,p(s(y)))
30:		PLUS(x,s(y))	→ P(s(y))
31:		TIMES(s(x),y)	→ PLUS(y,times(x,y))
32:		TIMES(s(x),y)	→ TIMES(x,y)
33:		DIV(x,y)	→ QUOT(x,y,y)
34:		QUOT(s(x),s(y),z)	→ QUOT(x,y,z)
35:		QUOT(x,0,s(z))	→ DIV(x,s(z))
36:		DIV(div(x,y),z)	→ DIV(x,times(y,z))
37:		DIV(div(x,y),z)	→ TIMES(y,z)
38:		EQ(s(x),s(y))	→ EQ(x,y)
39:		DIVIDES(y,x)	→ EQ(x,times(div(x,y),y))
40:		DIVIDES(y,x)	→ TIMES(div(x,y),y)
41:		DIVIDES(y,x)	→ DIV(x,y)
42:		PRIME(s(s(x)))	→ PR(s(s(x)),s(x))
43:		PR(x,s(s(y)))	→ IF(divides(s(s(y)),x),x,s(y))
44:		PR(x,s(s(y)))	→ DIVIDES(s(s(y)),x)
45:		IF(false,x,y)	→ PR(x,y)

The approximated dependency graph contains 5 SCCs: {38}, {26,27,29}, {32}, {33-36} and {43,45}.

Consider the SCC {38}. There are no usable rules. By taking the AF π with π(EQ) = 1 together with the lexicographic path order with empty precedence, rule 38 is strictly decreasing.

Consider the SCC {26,27,29}. The usable rules are {1}. By taking the AF π with π(p) = π(PLUS) = 1 together with the lexicographic path order with empty precedence, the rules in {27,29} are weakly decreasing and the rules in {1,26} are strictly decreasing. There is one new SCC.
- Consider the SCC {27,29}. The constraints could not be solved.

Consider the SCC {32}. There are no usable rules. By taking the AF π with π(TIMES) = 1 together with the lexicographic path order with empty precedence, rule 32 is strictly decreasing.

Consider the SCC {33-36}. The usable rules are {1-9}. The constraints could not be solved.

Consider the SCC {43,45}. The usable rules are {1-20}. The constraints could not be solved.

Tyrolean Termination Tool (0.34 seconds) --- May 3, 2006